es:ES, x, free:Id, n:, e:E.
@loc(e)(x:Id)
 (((x after e) = (x when e)  Id))
 (0 < n)
 (n  round(e))
 (e':E. (e' loc e  & rank(e') = <n, 0>  (:  ) & (((x after e') = (x when e')  Id)))) 

latex

Definitions

inc-snd(p), inc-fst(p), {T}, SQType(T), ff, tt, if b then t else f fi , Y, rank(e), t.1, round(e), P  Q, A c B, x. t(x), (e <loc e'), e loc e' , P & Q, x:A. B(x), A  B, A, @i(x:T), , t  T, P  Q, , x:A. B(x), let x = a in b(x), @e(xv), False, P  Q, Unit, , Dec(P), x(s), WellFnd{i}(A;x,y.R(x;y)),

Lemmas

nat sq, es-le transitivity, f-round-start, es-le weakening, es-locl transitivity1, es-le wf, not functionality wrt iff, assert-eq-id, eq id wf, f-rank wf, bool sq, bool cases, change-to-last-change, loc-last-change, last-change-property, last-change wf, assert of bnot, eqff to assert, bnot wf, iff transitivity, eqtt to assert, bool wf, id-deq wf, changed wf, decidable assert, es-le weakening eq, decidable int equal, es-causl wf, es-le-loc, es-locl wf, false wf, es-isconst wf, assert wf, es-locl-wellfnd, event system wf, es-E wf, Id wf, es-dtype wf, es-when wf, es-vartype wf, es-loc wf, es-after wf, not wf, nat wf, f-round wf, le wf